1 The Syntax of First-order Logic
2 The Semantics of First-order Logic
3 Sequent Calculus
4 Completeness of First-order Logic
In this section, we want to show the comleteness,which means :
$$ \text{If }\Phi \models \varphi\text{, then }\Phi \vdash \varphi $$We can paraphrase this statement to its contrapositive:
$$ \begin{align} &\Phi \not\vdash \varphi \text{ implies }\Phi \not\models \varphi \\ \iff& \text{if }\Phi \cap \{\neg\varphi\} \text{ is consistent, then } \Phi \cap\{\neg\varphi\} \text{ is satisfiable} \end{align} $$We can notice that any nonempty set can be paraphrased to $\Phi \cap \{\neg\varphi\}$, so we wil prove a general statement:
$$ \text{cons}(\Phi) \text{ implies } \Phi \text{ is satisfiable} $$Now for every consistent set, we need to find a model which satisfies this set.
We will use Henkin's Theorem to show that a set with some limits we can find this model. Then we will show that for any consistent set we can extend it to a set with these limits, so we find a model to satisfy this larger set, which must satisfy the consistent set without these limits.
4.1 Henkin’s Theorem
5 The Löwenheim-Skolem Theorem and the Compactness Theorem
6 Decidability and Enumerability
In this section, we want to
6.1 Decidability and Enumerability
Let $\mathcal{A}$ be an alphabet (always we assume it finite) and $\mathcal{W} \subset A^*$.
And what is procedure will be clarified afterwards.
6.1.1 Decidability
If there is a procedure will eventually halt and for every input $\mathcal{w} \in A^$,it can output some $\mathcal{w}\prime \in \mathcal{A}^$ such that
- if $\mathcal{w} \in \mathcal{W}$，then $\mathcal{w}\prime = \square$
- if $\mathcal{w} \not\in \mathcal{W}$，then $\mathcal{w}\prime \ne \square$
then $\mathcal{W}$ is decidable.
6.1.2 Enumerability
If there is a procedure that can output all words in $\mathcal{W}$ (in some order and repititions are admitted), then $\mathcal{W}$ is enumerable.
Furthermore, if there is a procedure that can output all words in $\mathcal{W}$, there is a procedure that can output all words in $\mathcal{W}$ without repetitions.
And let $\mathcal{A}$ is finite, then $\mathcal{A}^*$ is enumerable.
We define $S_{\infty}$:
$$ \begin{align} S_{\infty} \coloneqq & \{c_{0},c_{1}\dots\} & (c_{i}\text{ are constants}) \\ & \bigcup_{n \geq 1} \{R_{0}^n, R_{1}^n\dots\} & (R_{i}^n \text{ are n-ary relation symbols} ) \\ & \bigcup_{n \geq 1} \{f_{0}^n, f_{1}^n\dots\} & (f_{i}^n \text{ are n-ary function symbols} ) \end{align} $$and we have Lemma:
$$ \{\varphi \in L_{0}^{S_{\infty}} \mid \models \varphi\} \text{ is enumerable} $$$Proof:$ [sktech] By the completeness theorem, we know that:
$$ \{\varphi \in L_{0}^{S_{\infty}} \mid \models \varphi\} \iff \{\varphi \in L_{0}^{S_{\infty}} \mid \vdash \varphi\} $$Thus, we can enumerate all proofs of $S_{\infty}$, which must contain all $\varphi$ that $\vdash \varphi$
6.1.3 Relationship
Every decidable set is enumerable. We just need to show that a decidable set can be enumerated in some ways, and it's obvious : we can enumerate A*, and try to justify every word if it is in $\mathcal{W}$ and decide whether to output. And we successfully output all words in $\mathcal{W}$.
$\mathcal{W} \in A^, \mathcal{W}$ is decidable if and only if $\mathcal{W}$ and $A^ \setminus \mathcal{W}$ are both enumerable. From left to right, just apply last theorem. For the converse, we just need to simulate 2 procedure2 $\mathbb{P}_{1}$ and $\mathbb{P}_{2}$, and every $\mathcal{w}$ will appear in one's outputs.Then we successfully decide this set.
6.1.4 Computable Functions
We have a procedure, for every $\mathcal{w} \in \mathcal{A}^$ , apply this procedure on it and get $\mathcal{w} \in \mathcal{B}^$,which determines a function f, then f in computable.
6.2 Register Machines
6.2.1
Only 5 instructions.
-
-
-
-
-
这里应该是定义
6.2.2 R-decidable , R-enumerate and R-computable
6.3 Halting Problem
7 The Undecidability of First-order Logic
In this section, we want to show: the set $\{ \varphi \in L_{0}^{S_{\infty}} \mid \models \varphi \}$ is not R-deciable.
We have known that the halting problem is not R-deciable. So we want to show that halting problem can be reduced to this problem.
For every program $\mathbb{P}$, we try to construct a formula $\varphi_{\mathbb{P}} \in L_{0}^{S_{\infty}}$ such that:
$$ \mathbb{P} : \square \to \text{halt} \iff \models \varphi_{\mathbb{P}} $$To construct this, we introduce a concept: configurations.
-
-
-
讲格局是什么
8 Theories and Arithmetic
8.1 Theory
A theory $T \subseteq L_{0}^{S}$ is a set of sentences, and
- T is satisfiable
- T is closed under consequences, i.e., for every $\varphi \in L_{0}^{S}$, if $T \models \varphi$, then $\varphi \in T$
Let $\mathfrak{A}$ be an S-structure. Then $\text{Th}(\mathfrak{A}) \coloneqq \{ \varphi \in L_{0}^S \mid \mathfrak{A} \models \varphi\}$ is a theory.
Let $T \subseteq L_{0}^{S}$. We define $T^{\models} \coloneqq \{ \varphi \in L_{0}^{S} \mid T \models \varphi \}$
And the following 3 statements are equivalent
- $T^{\models}$ is a theory
- T is satisfiable
- $T^{\models} \not= L_{0}^{S}$
Let $T \subseteq L_{0}^{S}$ be a theory
- T is R-axiomatizable if there exists an R-deciable $\Phi \subseteq L_{0}^{S}$ with $T = \Phi^{\models}$
- T is finitely axiomatizable if there exists a finite $\Phi \subseteq L_{0}^{S}$ with $T=\Phi^{\models}$
Any finitely axiomatizable T is R-axiomatizable.
Exery R-axiomatizable theory is R-enumerable.(maybe need proof)
There are R-axiomatizable theories that are not R-deciable.
Let $S=S_{\infty},\Phi =\emptyset$, then
$$ \Phi^{\models} = \{ \varphi \in L^{S_{\infty}} \mid \models \varphi \} $$A theory $T \subseteq L_{0}^{S}$ is complete if for any $\varphi \in L_{0}^S$, either $\varphi \in T$ or $\neg \varphi \in T$.
Let $\mathfrak{A}$ be an S-structure. Then the theory $\text{Th}(\mathfrak{A})$ is complete.
Every R-axiomatizable complete theory $\text{Th}(\mathfrak{A})$ is complete
Every R-enumerable complete theory is R-deciable
8.2 Arithmetic
Let $\mathfrak{N} \coloneqq (\mathbb{N}, +,\cdot,0,1)$, $\text{Th}(\mathfrak{N})$ is called (elementary) arithmetic.
Peano Arithmetic：
Peano Arithmetic $\Phi_{PA}$ consists of the following $S_{ar}$-sentences ($S_{ar} = \{ +,\cdot,0,1 \}$)
- $\forall x \quad\neg x+1 \equiv 0$
- $\forall x \quad x+0 \equiv x$
- $\forall x \quad x \cdot 0 \equiv 0$
- $\forall x \forall y \quad (x+1\equiv y+1 \to x\equiv y)$
- $\forall x \forall y \quad x+(y+1) \equiv (x+y)+1$
- $\forall x \forall y x \cdot (y+1) \equiv x \cdot y + x$
and for all n $\in \mathbb{N}$, all variables $x_{1},\dots x_{n}, y$, and all $\varphi \in L^{S_{ar}}$ with free($\varphi$) $\subseteq \{ x_{1}\dots x_{n},y \}$,have
$$ \forall x_{1} \dots \forall x_{n} \left( \left(\varphi\frac{0}{y} \land \forall y\left( \varphi\to \varphi \frac{y+1}{y} \right)\right)\to \forall y \varphi \right) $$8.3 The Undecidability of Arithmetic
We want to show that $\text{Th}(\mathfrak{N})$ is not R-deciable. The core is still to reduce this problem to halting problem.
9 Gödel's Incompleteness Theorems
In this section, our goal is to prove three theorems:
- Tarski’s Undefinability of the Arithmetic Truth
- G¨odel’s First Incompleteness Theorem
- G¨odel’s Second Incompleteness Theorem
Using $\beta$-function, it is routine to prove :
Let $r\geq 1$
- Let $\mathscr{R} \subseteq \mathbb{N}^r$ be an R-decidable relation. Then there is an $L^{S_{ar}}$-formula $\varphi(v_{0},\dots,v_{r-1})$ ,such that for all $\mathscr{l}_{0},\dots,\mathscr{l}_{r-1} \in \mathbb{N}$
- Let f : $\mathbb{N}^r \to \mathbb{N}$ be an R-computable function. Then there is an $L^{S_{ar}}$-formula $\varphi(v_{0},\dots,v_{r-1},v_{r})$
Therefore,
$$ \mathfrak{N} \models \exists^{=1}v_{r} \varphi(\bar{\mathscr{l}}_{0},\dots,\bar{\mathscr{l}}_{r-1},v_{r}) $$where $\exists^{=1}x \theta(x)$ denotes the formula
$$ \exists x(\theta(x) \land \forall y(\theta(y)\to y\equiv x)) $$With these lemmas we can define representablility.
Let $\Phi \subseteq L_{0}^{S_{ar}}$ and $r\geq 1$
- A relation $\mathscr{R} \subseteq \mathbb{N}^{r}$ is representable in $\Phi$ if there is an $L^{S_{ar}}$-formula $\varphi(v_{0},\dots,v_{r-1})$ such that for all $n_{0},\dots,n_{r-1} \in \mathbb{N}$
- A function $F: \mathbb{N}^r \to \mathbb{N}$ is representable in $\Phi$ if there is an $L^{S_{ar}}$-formula $\varphi(v_{0},\dots,v_{r-1},v_{r})$ such that for all $n_{0},\dots,n_{r-1},n_{r} \in \mathbb{N}$
Moreover,
$$ \Phi \vdash \exists^{=1}v_{r}\varphi(\bar{n}_{0},\dots,\bar{n}_{r-1},v_{r}) $$So we can see these lemmas:
- If $\Phi$ is inconsistent, then every relation over $\mathbb{N}$ and every function over $\mathbb{N}$ is representable in $\Phi$.(which means, in an inconsistent $\Phi$, we can represent every formula.)
- Let $\Phi \subseteq \Phi^\prime \subseteq L_{0}^{S_{ar}}$. Then every relation representable in $\Phi$ is also representable in $\Phi$ is representable in $\Phi^\prime$ as well.
- Let $\Phi$ be consistent. If $\Phi$ is R-decidable,then every relation representable in $\Phi$ is R-decidable, and every function representable in $\Phi$ is R-computable.
And we define $\Phi$ allow representations if all R-decidable relations and all R-computable functions over $\mathbb{N}$ are representable in $\Phi$.
And we can see Th($\mathfrak{N}$) and $\Phi_{\text{PA}}$ both allow representations.
Then we want to allocate a G¨odel number for every $L^{S_{ar}}$ -formula.
It is easy to see $L^{S_{ar}}$-formulas are R-enumerable. So we can let
$$ \varphi_{0},\varphi_{1},\dots, $$be an effective enumeration of all $L^{S_{ar}}$ - formulas without repetition.Then for every $\varphi \in L^{S_{ar}}$ we let
$$ [\varphi] \coloneqq n \text{ where } \varphi = \varphi_{n} $$Observe that both
$$ n \mapsto \varphi_{n} \text{ and } \varphi \mapsto [\varphi] $$are R-computable.
Now we introduce an important theorem:
Fixed Point Teorem: Assume that $\Phi$ allows representations. Then for every $\psi\in L_{1}^{S_{ar}}$, there is an $S_{ar}$-sentence $\varphi$ such that
$$ \Phi \vdash \varphi \leftrightarrow \psi(\bar{[\varphi]}) $$proof:
We define that : Let $\Phi \subseteq L^{S_{ar}}$. Then
$$ \Phi^{\vdash} \coloneqq \{ \varphi \in L^{S_{ar}} \mid \Phi \vdash \varphi \} $$We say that $\Phi^{\vdash}$ is representable in $\Phi$ if
$$ \{ [\varphi] \in \mathbb{N} \mid \varphi \in \Phi^{\vdash} \} = \{ [\varphi] \mid \varphi \in L^{S_{ar}}\text{ and } \Phi \vdash \varphi \} $$And we can see a Lemma :
Let $\Phi \subseteq L^{S_{ar}}$ be consistent and allow representations. Then $\Phi^{\vdash}$ is not representable in $\Phi$.
proof:
Assume that $\Phi^{\vdash}$ is representable in $\Phi$. In particular, there is a $\mathcal{X}(v_{0})\in L_{1}^{S_{ar}}$ such that for all $\varphi \in L_{0}^{S_{ar}}$
$$ \begin{align} \Phi \vdash \varphi \implies \Phi \vdash \mathcal{X}(\bar{[\varphi]}), \\ \Phi \not\vdash \varphi \implies \Phi \vdash \neg\mathcal{X}(\bar{[\varphi]}) \end{align} $$Since $\Phi$ is consistent, we conclude
$$ \Phi \not\vdash \varphi \iff \Phi \vdash \neg \mathcal{X}(\bar{[\varphi]}) $$We apply the Fixed Point Theorem to $\neg \mathcal{X}$ to obtain a sentence $\varphi$ such that
$$ \Phi \vdash \varphi \leftrightarrow \neg \mathcal{X}(\bar{[\varphi]}) $$We can easily see a contradiction.
Then we can easily see
Tarski’s Undefinability of the Arithmetic Truth:
- Let $\Phi \subseteq L^{S_{ar}}$ be consistent and allow representations. Then $\Phi^{\models}$ is not representable in $\Phi$.
- Th($\mathfrak{N}$) is not representable in Th($\mathfrak{N}$).
The proof is obvious.
G¨odel’s First Incompleteness Theorem:
Let $\Phi \subseteq L^{S_{ar}}$ be consistent and allow representations. Moreover, $\Phi$ is R-decidable. Then there is an $L^{S_{ar}}$-sentence $\varphi$ such that neither $\Phi \vdash \varphi$ nor $\Phi \vdash \neg \varphi$.
Proof:
Assume for every $L^{S_{ar}}$-sentence $\varphi$ either $\Phi \vdash \varphi$ or $\Phi \vdash \neg \varphi$. Thus $\Phi$ is complete. By the R-decidability of $\Phi$ , we can then conclude that $\Phi^{\vdash}$ is R-dicidable too.
Since $\Phi$ allows representations, $\Phi^{\vdash}$ is representable in $\Phi$.
Then this is contradict to the Lemma. Then the proof ends.
Now we just know there is a $\varphi$ satisfy the conditions. To proof the G¨odel’s Second Incompleteness Theorem, we need to fix a R-decidable $\Phi \subseteq L_{0}^{S_{ar}}$ which allows representations and find a such $\varphi$.
We choose an effective enumeration of all derivations in the sequent calculus associated with $S_{ar}$ and define a relation $\mathscr{H} \subseteq \mathbb{N}^{2}$ by
$$ \begin{align} (n,m) \in \mathscr{H} \iff & \text{the m-th derivation in the above eunmeration ends with a sequent} \\ & \psi_{0},\dots ,\psi_{k-1},\varphi \text{ with } \psi_{0},\dots,\psi_{k-1} \in \Phi \text{ and }n=[\varphi] \end{align} $$Clearly, $\mathscr{H}$ is R-decidable by the R-decidability of $\Phi$. Moreover, for every $\varphi \in L^{S_{ar}}$
$$ \Phi \vdash \varphi \iff \text{there is an }m\in \mathbb{N} \text{ with }([\varphi],m)\in \mathscr{H} $$Since $\Phi$ allows representation, there is a $\varphi_{\mathscr{H}}(v_{0},v_{1}) \in L_{2}^{S_{ar}}$ such that for every $n,m \in \mathbb{N}$
$$ \begin{align} (n,m) \in \mathscr{H} \implies \Phi \vdash \varphi_{\mathscr{H}}(\bar{n},\bar{m}) \\ (n,m) \not\in \mathscr{H} \implies \Phi \vdash \neg\varphi_{\mathscr{H}}(\bar{n},\bar{m}) \end{align} $$We set
$$ \text{DER}_{\Phi}(x) \coloneqq \exists y\varphi_{\mathscr{H}}(x,y) $$which intuitively says that x is provable in $\Phi$.
Applying Fixed Point Theorem to $\psi(x) \coloneqq \neg\text{DER}_{\varphi}(x)$,we obtain an $L_{0}^{S_{ar}}$-sentence $\varphi$ such that
$$ \Phi \vdash \varphi \leftrightarrow \neg\text{DER}_{\varphi}(\bar{[\varphi]}) $$then we have lemma: $\text{Cons}(\Phi) \to \Phi \not\vdash \varphi$
and we observe that $\Phi \vdash 0\equiv 0$, therefore
$$ \Phi \text{ is consistent} \iff \Phi \not\vdash \neg 0\equiv 0 $$Hence,
$$ \text{CONS}_{\Phi} \coloneqq \neg \text{DER}([\neg 0\equiv 0]) $$Then we have another lemma:
Assume $\Phi_{\text{PA}} \subseteq \Phi$. Then
$$ \Phi \vdash \text{CONS}_{\Phi} $$G¨odel’s Second Incompleteness Theorem:
Assume $\Phi$ is consistent and R-decidable with $\Phi_{\text{PA}} \subseteq \Phi$ . Then
$$ \Phi \vdash \neg \text{DER}_{\Phi}([\varphi]) $$